r:. has-value(r) 

latex

Definitions	P  Q, t  T, has-value(a), x:A. B(x), if b then t else f fi , , A  B,
Lemmas	int nzero wf, btrue wf, bool wf, qeq wf, rationals wf